One of the major themes in data mining is the extraction of patterns existent in a data set. For example, data mining algorithms have been commissioned to recognize correlations in purchase patterns of consumers. For instance, a data mining algorithm can be employed to ascertain that an individual will generally purchase toothpaste if the individual also purchased a toothbrush. In another example, a data mining algorithm can be commissioned to infer sequential patterns in data. If an individual purchases a shirt, for instance, the data mining algorithm can infer that the individual will likely purchase trousers after purchasing the shirt. Such correlations in transactions can be useful in connection with product placement, marketing, etc.
Conventionally, however, data mining techniques have not been widely utilized in connection with software verification tools. For example, given a program and documented rules/constraints imposed by developers on the program, software verification tools can be utilized to verify that the program satisfies the rules/constraints imposed by the developers. For instance, software verification tools can be employed to ascertain that a program that uses a library/application programming interface does so in accordance with rules/constraints of the library/application programming interface. The usefulness of such verification tools, however, is limited due to lack of machine-readable rules/constraints for programs. For instance, with respect to legacy software, developer turnover can result in the loss of a substantial amount of knowledge about the internal workings of the software that is ingrained in the memory of developers but is not written in a specification pertaining to the software. While documentation may curb some of such losses, oftentimes internal details of software are conventionally not documented.
In another example, alteration to undocumented but observed behaviors of software can cause clients of the software to fail as such software evolves. These failures can be alleviated if rules/constraints of the software are available to developers at the time they make modifications to such software.